| Definitions | Raframe-k(x1), P   Q, t  T, Rbframe-k(x1), ( x,yL.P(x;y)), DeclaredType(ds;x), IdDeq, tl(l), {i..j }, R-Feasible(R),   b, Rsends-ds(x1), onceR{$a:ut2, $done:ut2}(i), {T}, Rsends?(x1), True, Rbframe-L(x1), Rsends-g(x1), Rpre?(x1), p  q, Rsends-dt(x1), Rplus-left(x1), R-interface-compat(A;B), A & B, Reffect-x(x1), Reffect?(x1), Rsframe?(x1), SQType(T), Reffect-ds(x1), Rrframe-L(x1), false, P & Q, i j, Rsends-l(x1), i<j, 2of(t), nth_tl(n;as), Rda(R), Rsframe-tag(x1), Rframe-x(x1), Rplus-right(x1), Rrframe?(x1), i j < k, if b t else f fi, Reffect-knd(x1), true, Rsends-T(x1), Raframe?(x1), R-base-domain(R), l[i], i=j, xL. P(x), x:A. B(x), hd(l), Rsframe-L(x1), Rbframe?(x1), AB, Rpre-a(x1), Rrframe-x(x1), Top, Reffect-T(x1), A || B, s.x,  x. t(x), 1of(t), Rframe?(x1), Y, A, Rds(R), False, R-frame-compat(A;B), Rsframe-lnk(x1), R-loc(R), Raframe-L(x1), "$x", Prop, Normal(T), ||as||, Atom2Deq, Rsends-knd(x1), a = b, p = q, Rpre-ds(x1), eq_atom$n(x;y), Rplus?(x1), eqof(d), Rframe-L(x1), Rnone?(x1), Dec(P), (x l), x(s), isrcv(k),  x:A. B(x), Id,  , Unit,  b,  , Realizer, State(ds), isl(x), P  Q, locl(a), P  Q,  |